Can you include the implication (and maybe prove it) that 1145 => 28?

Thanks especially for clarifying the problem by asking a question on erdosproblems.com!

Can you include the implication (and maybe prove it) that 1145 => 28?

@[category research open, AMS 5]
theorem erdos_1145 :
  ∀ ⦃A B : Set ℕ⦄ (hA : A.Infinite) (hB : B.Infinite),
    Tendsto (fun n ↦ (Nat.nth (· ∈ A) n : ℝ) / (Nat.nth (· ∈ B) n : ℝ)) atTop (𝓝 1) →
    (∀ᶠ n in atTop, n ∈ A + B) →
    limsup (fun n => ↑(((𝟙_A ∗ 𝟙_B) : ℕ → ℕ) n)) atTop = (⊤ : ℕ∞) := by
  sorry

/--
If $A ⊆ \mathbb{N}$ is such that $A + A$ contains all but finitely many integers then
 $\limsup 1_A ∗ 1_A(n) = \infty$.
-/
@[category research open, AMS 11]
theorem erdos_28  (A : Set ℕ) (h : (A + A)ᶜ.Finite) :
    limsup (fun (n : ℕ) => (sumRep A n : ℕ∞)) atTop = (⊤ : ℕ∞) := by
  sorry

@[category test, AMS 11]
theorem test : type_of% erdos_1145 → type_of% erdos_28 := by
  delta sumRep
  use fun and K V=>V.exists_le.elim fun R L=>by_contra fun and' =>?_
  by_cases h:K.Finite
  · use(h.add h).infinite_compl V
  · bound[and h h (tendsto_atTop_of_eventually_const fun and p=>div_self (mod_cast (ne_of_gt (p.trans ((Nat.nth_strictMono h)).le_apply)))) ((Filter.eventually_gt_atTop R).mono fun and=>not_imp_comm.1 (L _) ∘not_le_of_lt)]

is a start for this (proof by AlphaProof)

I removed the answer(sorry), which only 1145 should have, so needs to be put back there, but then it is probably a good idea to define a Prop for erdos 1145, to make it easier.
Then one needs to decide which way around we import the definitions (probably better to do everything in the 1145 file?
Also I removed the hypothesis that those sets start at zero, not sure if this makes any difference, but in 28 we didn't have the condition!

In any case, @danielchin please either do that here, or add a TODO, so we can add it at some later point!

Added the implication here. The only change I had to make to the AlphaProof proof was changing not_le_of_lt to not_le_of_gt due to a deprecation warning of not_le_of_lt.

From an organizational standpoint, I would think it makes more sense to keep problem 28 in 28.lean and just import it into 1145.lean. It also looks like problem 40 is a stronger version of 28, so if we were to add the implication of 40 => 28, it would be easier to leave 28 where it is now instead of doing a roundabout way to get to 28 through 1145.lean.

The only thing I'm not worried about is how we dropped the condition that A and B don't contain 0. Does this make any difference in the problem? In any case, now there is a difference between the docstring (which should also be duplicated for the Prop, btw) and the lean code. Either change the lean code back to include the condition (preferred!, but perhaps hard to make work with the relation to erdos28) or explain in the docstring if it doesn't matter.

I went back and forth on this one for a day. It looks like the implication from a zero excluded 1145 to 28 is possible, but it starts blowing up the proof in size to the point where it's probably not worth it to keep in this repository (I also never got to a point where it compiled properly).

There's also discussion on the Erdos problem website under the comments of both 1145 and 28 discussing whether should be included for both of the problems. And it seems like T. Bloom has made it a bit ambiguous on purpose. 1145 was originally written as $A + B = \mathbb{N}$ (according to Woett's comment in 28), which would imply 0 was included. And T. Bloom's comment in 1145, implies that 1145 could be interpreted as 0 could be included or we could treat it as "it holds for sufficiently large integers". So all in all ¯_(ツ)_/¯

Left a docstring describing the above.